Nuprl Lemma : concat-is-nil
11,40
postcript
pdf
T
:Type,
LL
:(
T
List List). (concat(
LL
) = []
(
T
List))
(
L
LL
.
L
= []
(
T
List))
latex
Definitions
t
T
,
x
L
.
P
(
x
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
,
x
.
t
(
x
)
,
P
Q
,
P
Q
,
P
&
Q
,
concat(
ll
)
,
as
@
bs
Lemmas
append
is
nil
,
append
wf
,
iff
functionality
wrt
iff
,
l
all
cons
,
concat
wf
,
l
all
wf
,
l
all
nil
origin
T:Type, LL:(T List List). (concat(LL) = [] 
(T List)) 
(LLL. L = [] (T List)) T:Type, LL:(T List List). (concat(LL) = [] (T List)) (LLL. L = [] (T List)) TxL. P(x) Qx:A. B(x)
x. t(x) Q Q